package main;
import java.util.Arrays;
import java.util.Vector;

public class Encoder {
	
	public static Vector<int[]> atLeastOne(int[] lits){
		int[] l = Arrays.copyOf(lits, lits.length);
		Vector<int[]> res = new Vector<int[]>();
		res.add(l);
		return res;
	}
	
	public static int[][] atMostOne(int[] lits){
		int dimension = lits.length;
		int[][] res = new int[(int) dimension*(dimension-1)/2][2];
		
		int counter = 0; 
		for (int i = 0; i < dimension; i++){
			for (int j = i+1; j < dimension; j++){
				int[] p = new int[2];
				p[0] = -lits[i];
				p[1] = -lits[j];
				res[counter++] = p;
			}
			
		}
		return res;
	}
	
	public static int[][] xor2(int s, int lit1, int lit2){
		int[][] cnf = new int[4][3];
		// CNF representing the "false" table of the expression lit1 <-> lit2 XOR lit3 
		cnf[0] = new int[]{-s, -lit1, -lit2}; 
		cnf[1] = new int[]{-s, lit1, lit2};
		cnf[2] = new int[]{s, -lit1, lit2};
		cnf[3] = new int[]{s, lit1, -lit2};
		return cnf;
	}
	
	
	
	public static int[][] xor3(int lit1, int lit2,int lit3, int s0){
		int[][] cnf = new int[8][4];	
		cnf[0] = new int[]{lit1,lit2,lit3,-s0};
		cnf[1] = new int[]{lit1,lit2,-lit3,s0};
		cnf[2] = new int[]{lit1,-lit2,lit3,s0};
		cnf[3] = new int[]{lit1,-lit2,-lit3,-s0};
		cnf[4] = new int[]{-lit1,lit2,lit3,s0};
		cnf[5] = new int[]{-lit1,lit2,-lit3,-s0};
		cnf[6] = new int[]{-lit1,-lit2,lit3,-s0};
		cnf[7] = new int[]{-lit1,-lit2,-lit3,s0};
		return cnf;
	}
	
	public static int[][] cOut(int lit1, int lit2,int lit3, int s1){
		int[][] cnf = new int[8][4];	
		cnf[0] = new int[]{-lit1,-lit2,-lit3,s1};
		cnf[1] = new int[]{-lit1,-lit2,lit3,s1};
		cnf[2] = new int[]{-lit1,lit2,-lit3,s1};
		cnf[3] = new int[]{-lit1,lit2,lit3,-s1};
		cnf[4] = new int[]{lit1,-lit2,-lit3,s1};
		cnf[5] = new int[]{lit1,-lit2,lit3,-s1};
		cnf[6] = new int[]{lit1,lit2,-lit3,-s1};
		cnf[7] = new int[]{lit1,lit2,lit3,-s1};
		return cnf;
	}
	
	public static int[] fullAdder(int[] lits, LiteralAlocatorAndMap map, Vector<int[]> cnf){
		int[] sumBinaryLits = null;
		int zeroLit = map.getZeroLit();
		
		if (lits.length <=3){
			// S1 = A xor B xor C
			// S2 = AB + C(A xor B)
			int s1 = map.newOther("s1");
			int s2 = map.newOther("s2");
			sumBinaryLits = new int[]{s1,s2};
			int[][] cnfAddition = xor3(lits[0],lits[1],lits.length<3?zeroLit:lits[2],s1);
			for (int[] is : cnfAddition) {
				cnf.add(is);
			}
			cnfAddition = cOut(lits[0],lits[1],lits.length<3?zeroLit:lits[2],s2);
			cnf.addAll(Arrays.asList(cnfAddition));
		}
		else{
			int[] litsL = Arrays.copyOfRange(lits, 0, lits.length/2);
			int[] litsR = Arrays.copyOfRange(lits, lits.length/2, lits.length);
			int[] resL = fullAdder(litsL, map, cnf);
			int[] resR = fullAdder(litsR, map, cnf);
			int maxSize = Math.max(resL.length, resR.length);
			resL = padWithZero(zeroLit, resL, maxSize);
			resR = padWithZero(zeroLit, resR, maxSize);
			sumBinaryLits = sum2numbers(resL, resR, zeroLit, map, cnf);
			
		}
		return sumBinaryLits;
	}

	
	/**
	 * assuming the 2 numbers has the same number of bits
	 * @param resL
	 * @param resR
	 * @param cnf 
	 * @param map, 
	 * @return
	 */
	private static int[] sum2numbers(int[] resL, int[] resR, int zero, LiteralAlocatorAndMap map, Vector<int[]> cnf) {
		int c_in =zero; 
		int[] res = new int[resL.length+1];
		for (int i = 0; i < resR.length; i++) {
			int[] lits = {c_in,resL[i],resR[i]};
			int[] newLits = fullAdder(lits, map, cnf);
			c_in = newLits[1];
			res[i] = newLits[0];
		}
		res[res.length-1] = c_in;
		return res;
	}

	private static int[] padWithZero(int zero, int[] lits,
			int maxSize) {
		if (lits.length < maxSize){
			int oldLength = lits.length;
			lits = Arrays.copyOf(lits, maxSize);
			for (int i = oldLength; i < lits.length; i++) {
				lits[i] = zero;
				
			}
		}
		return lits;
	}

	public static Vector<int[]> atLeastOneFalse(int[] lits){
		int[] l = Arrays.copyOf(lits, lits.length);
		for (int i = 0; i < l.length; i++) {
			l[i] = -l[i];
		}
		return atLeastOne(l);
	}
	
}
